Forcing interpretation, conservation and proof size

Abstract:

The notion of relative interpretation is one of the essential tools of proof theory. In [1], Avigad demonstrated how forcing can be understood in the context of proof theory and how it is related to relative consistency or conservation proofs. Indeed, one may see that forcing is a generalization of a relative interpretation by means of the Kripke semantics.

Moreover, such an interpretation usually provides a feasible (polynomial) proof transformation as digested in [2]. In this talk, we will overview such ideas and show that many conservation theorems for systems of second-order arithmetic can be converted to non-speedup theorems.

[1] J. Avigad, Forcing in proof theory. Bull. Symbolic Logic 10 (2004), no. 3, 305-333.
[2] J. Avigad, Formalizing forcing arguments in subsystems of second-order arithmetic. Ann. Pure Appl. Logic 82 (1996), no. 2, 165-191.
[3] L. A. Kolodziejczyk, T. L. Wong and K. Yokoyama, Ramsey's theorem for pairs, collection, and proof size, submitted.

logic in computer sciencelogic

Audience: researchers in the topic

Proof Theory Virtual Seminar

Series comments: The Proof Theory Virtual Seminar presents talks by leading researchers from all areas of proof theory. Everyone who is interested in the subject is warmly invited to attend! In order to participate, please visit the seminar webpage: www.proofsociety.org/proof-theory-seminar/